fact: Fixpoint hlist_rev' ls ls' (h : hlist ls) : hlist ls' -> hlist (rev ls ++ ls') := match h in hlist ls return hlist ls' -> hlist (rev ls ++ ls') with | Hnil => fun h => h | Hcons l ls0 x h' => fun hacc => match app_ass_trans (rev ls0) (l :: nil) ls' in _ = t return hlist t -> hlist _ with | eq_refl => fun x => x end (@hlist_rev' _ (l :: ls') h' (Hcons x hacc)) 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