proposition: Lemma app_nil_r_trans : forall {T : Type} (a : list T), a ++ nil = a.
proof: Proof. induction a; simpl. reflexivity. refine match IHa in _ = X return _ = _ :: X with | eq_refl => eq_refl end. Defined.
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