proposition: Lemma Hcons_inv : forall l ls a b c d, @eq (hlist (l :: ls)) (Hcons a b) (Hcons c d) -> a = c /\ b = d.
proof: Proof. intros. refine ( match H as K in _ = Z return match Z in hlist LS return match LS with | nil => Prop | l :: ls => F l -> hlist ls -> Prop end with | Hcons X Y x y => fun a b => a = x /\ b = y | Hnil => True end a b with | eq_refl => conj eq_refl eq_refl end). Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.Member ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics Coq.Classes.Morphisms