proposition: Lemma methodType_to_funType_id {rep : Type} {dom : list Type} {cod : Type} (f : funType (rep :: dom) (rep * cod)) : methodType_to_funType (funType_to_methodType f) = f.
proof: Proof. unfold methodType_to_funType, funType_to_methodType. extensionality r. induction dom; simpl in f; extensionality x; simpl. reflexivity. exact (IHdom (fun r => f r x)). Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT Fiat.ADTNotation Fiat.Computation.FixComp Coq.ZArith.ZArith Coq.Arith.PeanoNat