proposition: Lemma app_aeq_l : forall v1 v2 t, App v1 v2 ~~ t -> exists u1 u2, t = App u1 u2 /\ u1 ~~ v1 /\ u2 ~~ v2.
proof: Proof. intros v1 v2 t e. apply app_aeq_r. sym. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)