proposition: Lemma lam_aeq_r : forall t x u, t ~~ Lam x u -> exists y v, t = Lam y v /\ v ~~ rename x y u /\ (x = y \/ ~In y (fv u)).
proof: Proof. cut (forall t t', t ~~ t' -> forall x u, t = Lam x u \/ t' = Lam x u -> exists y v, v ~~ rename x y u /\ (x=y \/ ~In y (fv u)) /\ (t = Lam x u -> t' = Lam y v) /\ (t' = Lam x u -> t = Lam y v)). intros h t x u e. assert (p : t = Lam x u \/ Lam x u = Lam x u). auto. destruct (h _ _ e _ _ p) as [y [v i]]. ex y v. tauto. induction 1; intros z a e. ex z a. split. rewrite rename_id. refl. tauto. rewrite or_sym in e. destruct (IHaeq _ _ e) as [y [w i]]. ex y w. tauto. destruct e as [e|e]. assert (p : u = Lam z a \/ v = Lam z a). auto. destruct (IHaeq1 _ _ p) as [x [b [i1 [i2 [i3 i4]]]]]. assert (q : v = Lam x b \/ w = Lam x b). tauto. destruct (IHaeq2 _ _ q) as [y [c [j1 [j2 [j3 j4]]]]]. ex y c. repeat split. rewrite j1, i1. apply rename2. hyp. destruct i2; destruct j2. left. trans x; auto. right. rewrite H1, rename_id in i1. rewrite <- i1. hyp. right. rewrite <- H2. hyp. eq_dec z y. auto. right. intro hy. apply H2. rewrite i1, fv_rename; unfold replace. destruct (mem z (fv a)); set_iff; auto. tauto. intro hw. subst u w. tauto. assert (p : v = Lam z a \/ w = Lam z a). auto. destruct (IHaeq2 _ _ p) as [x [b [i1 [i2 [i3 i4]]]]]. assert (q : u = Lam x b \/ v = Lam x b). tauto. destruct (IHaeq1 _ _ q) as [y [c [j1 [j2 [j3 j4]]]]]. ex y c. repeat split. rewrite j1, i1. apply rename2. hyp. destruct i2; destruct j2. left. trans x; auto. right. rewrite H1, rename_id in i1. rewrite <- i1. hyp. right. rewrite <- H2. hyp. eq_dec z y. auto. right. intro hy. apply H2. rewrite i1, fv_rename; unfold replace. destruct (mem z (fv a)); set_iff; auto. intro hu. subst u w. tauto. tauto. destruct e; discr. destruct e; discr. destruct e as [e|e]; inversion e; subst. ex z u'. rewrite rename_id. intuition. ex z u. rewrite rename_id. intuition. destruct e as [e|e]. inversion e. subst. ex y (rename z y a). split_all. refl. inversion e. subst. ex x u. rewrite rename2, rename_id. 2: auto. split_all. refl. rewrite fv_rename; unfold replace. case_eq (mem x (fv u)); [rewrite <- mem_iff|rewrite <- not_mem_iff]; intro hx. right. set_iff. intros [h|h]. subst z. tauto. tauto. auto. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)