proposition: Lemma hlist_app_nil_r : forall ls (h : hlist ls), hlist_app h Hnil = match eq_sym (app_nil_r_trans ls) in _ = t return hlist t with | eq_refl => h end.
proof: Proof. induction h; simpl; intros; auto. rewrite IHh at 1. unfold eq_trans. unfold f_equal. unfold eq_sym. clear. revert h. generalize dependent (app_nil_r_trans ls). 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