proposition: Lemma hlist_eta : forall ls (h : hlist ls), h = match ls as ls return hlist ls -> hlist ls with | nil => fun _ => Hnil | a :: b => fun h => Hcons (hlist_hd h) (hlist_tl h) end h.
proof: Proof. intros. destruct h; auto. 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