proposition: Lemma app_assoc_rw: forall L1 L2 L3, Equiv (App L1 (App L2 L3)) (App (App L1 L2) L3).
proof: Proof. intros. split; intros. - apply app_assoc_in_1. assumption. - apply app_assoc_in_2. assumption. Qed.
imports: Coq.Lists.List