(The topic looks similar to Inequality between Types, but the question is quite different.)

Say that I’ve defined two isomorphic types:

```
Parameter A B : Type.
Parameter A2B : A -> B.
Coercion A2B : A >-> B.
Parameter B2A : B -> A.
Coercion B2A : B >-> A.
```

and two polymorphic types:

```
Variant E : Type -> Type := aE : E A.
Variant E' : Type -> Type := bE : E' B.
```

Can I show that `E`

and `E'`

are by some means the same? *e.g.*

```
Goal forall T, E T -> E' T.
intros _ [].
```

Now I need to present an instance for `E' A`

. Is this feasible?