nqed.
nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
#T; #a; #l; #l1;
nrewrite > (associative_list T l [a] l1);
nnormalize;
nqed.
nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
#T; #a; #l; #l1;
nrewrite > (associative_list T l [a] l1);
nnormalize;