proposition: Lemma hlist_nil_eta : forall (h : hlist nil), h = Hnil.
proof: Proof. intros; rewrite (hlist_eta h); reflexivity. 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