that is parameterized to distinguish input, output and internal actions. I want to have a proof about that if we have some element a:action Input it must be of structure (inputEvent n l s n1 n2). So i assume something like this:

Lemma action_Input_is_inputEvent : forall (n : nat) (ts : list types) (name : string) (tid : nat) (sid : nat) (a : action Input),
a = inputEvent n ts name tid sid.

I tried to have a proof:

intros n ts name tid sid a.
induction a.

But this give me the error: The 3rd term has type “action Input” which should be coercible to “action i0”.
For me it seems that we cannot apply induction here, because not all cases are well-typed. Is there a way to have this kind of Lemma proven in Coq ? Or is there maybe a smarter way to define my datatype to make it more easy? Thank you!

I want to have a proof about that if we have some element a:action Input it must be of structure (inputEvent n l s n1 n2).

To express this, do not use forall but exists:

Lemma action_Input_is_inputEvent : forall (a : action Input), exists (n : nat) (ts : list types) (name : string) (tid : nat) (sid : nat),
a = inputEvent n ts name tid sid.

Then, dependency makes indeed that induction, or destruct, or inversion, or dependent inversion, or case_eq, … don’t work. However, dependent destruction works: