proposition: Lemma hlist_app_assoc : forall ls ls' ls'' (a : hlist ls) (b : hlist ls') (c : hlist ls''), hlist_app (hlist_app a b) c = match eq_sym (app_ass_trans ls ls' ls'') in _ = t return hlist t with | eq_refl => hlist_app a (hlist_app b c) end.
proof: Proof. intros ls ls' ls''. generalize (eq_sym (app_assoc_reverse ls ls' ls'')). induction ls; simpl; intros. { rewrite (hlist_eta a); simpl. reflexivity. } { rewrite (hlist_eta a0). simpl. inversion H. erewrite (IHls H1). unfold f_equal. unfold eq_trans. unfold eq_sym. generalize (app_ass_trans ls ls' ls''). rewrite <- H1. clear. intro. generalize dependent (hlist_app (hlist_tl a0) (hlist_app b c)). destruct e. 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