proposition: Lemma app_aeq_r : forall t v1 v2, t ~~ App v1 v2 -> exists u1 u2, t = App u1 u2 /\ u1 ~~ v1 /\ u2 ~~ v2.
proof: Proof. cut (forall t u, t ~~ u -> forall v1 v2, (t = App v1 v2 \/ u = App v1 v2) -> exists u1 u2, u1 ~~ v1 /\ u2 ~~ v2 /\ (t = App v1 v2 -> u = App u1 u2) /\ (u = App v1 v2 -> t = App u1 u2)). intros h v u1 u2 e. assert (p : v = App u1 u2 \/ App u1 u2 = App u1 u2). tauto. destruct (h _ _ e _ _ p) as [a [b [h1 [h2 [h3 h4]]]]]. ex a b. intuition. induction 1; intros u1 u2 e. ex u1 u2. firstorder auto with crelations. rewrite or_sym in e. destruct (IHaeq _ _ e) as [a [b [h1 [h2 [h3 h4]]]]]. ex a b. fo. destruct e. assert (p1 : u = App u1 u2 \/ v = App u1 u2). tauto. destruct (IHaeq1 _ _ p1) as [a [b [h1 [h2 [h3 h4]]]]]. assert (p2 : v = App a b \/ w = App a b). tauto. destruct (IHaeq2 _ _ p2) as [c [d [i1 [i2 [i3 i4]]]]]. ex c d. split_all; subst; try inversion H4; try inversion H5; try inversion H6; try inversion H2; subst; auto; try (trans a; hyp); try (trans b; hyp). assert (p2 : v = App u1 u2 \/ w = App u1 u2). tauto. destruct (IHaeq2 _ _ p2) as [a [b [h1 [h2 [h3 h4]]]]]. assert (p1 : u = App a b \/ v = App a b). tauto. destruct (IHaeq1 _ _ p1) as [c [d [i1 [i2 [i3 i4]]]]]. ex c d. split_all; subst; try inversion H2; try inversion H4; try inversion H5; subst; auto; try (trans a; hyp); try (trans b; hyp). destruct e as [h|h]; inversion h; subst; clear h. ex u' u2. firstorder auto with crelations. ex u u2. firstorder auto with crelations. destruct e as [h|h]; inversion h; subst; clear h. ex u1 v'. firstorder auto with crelations. ex u1 v. firstorder auto with crelations. destruct e; discr. destruct e; discr. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)