fact: Fixpoint hlist_app ll lr (h : hlist ll) : hlist lr -> hlist (ll ++ lr) := match h in hlist ll return hlist lr -> hlist (ll ++ lr) with | Hnil => fun x => x | Hcons _ _ hd tl => fun r => Hcons hd (hlist_app tl r) end.
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