proposition: Lemma hlist_app_assoc' : forall (ls ls' ls'' : list iT) (a : hlist ls) (b : hlist ls') (c : hlist ls''), hlist_app a (hlist_app b c) = match app_ass_trans ls ls' ls'' in (_ = t) return (hlist t) with | eq_refl => hlist_app (hlist_app a b) c end.
proof: Proof. clear. intros. generalize (hlist_app_assoc a b c). generalize (hlist_app (hlist_app a b) c). generalize (hlist_app a (hlist_app b c)). destruct (app_ass_trans ls ls' ls''). simpl. 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