proposition: Lemma cp_lam P Q : cp_aeq P -> cp_red P -> cp_sn P -> cp_neutral P -> cp_aeq Q -> cp_red Q -> cp_sn Q -> cp_neutral Q -> forall x u, (forall v, P v -> Q (subs (single x v) u)) -> arr P Q (Lam x u).
proof: Proof. intros P_aeq P_red P_sn P_neu Q_aeq Q_red Q_sn Q_neu x u hu. cut (SN R_aeq u). 2:{ apply Q_sn. rewrite <- (single_id x). apply hu. apply cp_var; hyp. } intro u_sn. revert u u_sn hu. induction 1; rename x0 into u; intros hu v hv. apply cp_app with (P:=P); auto. right. ex x u. refl. 2:{ intros x' u' e; inversion e; clear e; subst. fo. } intros t r. gen r; intro r'. apply lam_R_aeq_l in r'. destruct r' as [[t' [h1 [h2 h3]]]|[y [w [h1 h2]]]]; subst. intros a ha. assert (e : App t a ~~ subs (single x a) (App t' (Var x))). simpl. rewrite single_eq, single_notin_fv, h3. refl. hyp. rewrite e; clear e. apply hu. hyp. assert (h : y=x \/ ~In x (fv w)). eq_dec x y. auto. right. intro hx. apply fv_clos_aeq in r. 2: class. simpl in r. assert (i : In x (remove y (fv w))). set_iff. fo. apply r in i. revert i. set_iff. fo. rewrite aeq_alpha' with (y:=x). 2: hyp. apply H0. hyp. intros a ha. eapply proper_atc. class. apply Q_red. eapply subs_atc. class. refl. apply at_step. apply h2. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)