Defining different equality types as inductive types in Coq

user_3101967 0
Viewed 507

I am trying to define in Coq different types of equalities. During an university course my professor gave us the rules of four different types, as follows (I provide just the links to the rules):

The difference among these four types relies on the type C.

I am trying to prove the isomorphism among them. Unfortunately I have some troubles in declaring as inductive types the first and the second, because I cannot find a way to specify the type C. I have a definition for the third and the fourth, and I already proved the isomorphism between them.

Thanks in advance.

coq-tactic coq equality
1 Answers
Related