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.
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!