(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' 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?