proposition: Lemma cp_app P Q : cp_aeq P -> cp_red P -> cp_sn P -> cp_aeq Q -> cp_red Q -> cp_neutral Q -> forall t, (neutral t \/ exists x u, t = Lam x u) -> (forall t', t =>R t' -> arr P Q t') -> forall v, P v -> (forall x u, t = Lam x u -> Q (subs (single x v) u)) -> Q (App t v).
proof: Proof. intros P_aeq P_red P_sn Q_aeq Q_red Q_neu t t_neu_or_abs t_red_comp v0 v0_sn tv0_beta_comp. set (B := fun v => v0 =>R* v -> Q (App t v)). cut (B v0). intro h. apply h. refl. set (S := RelUtil.restrict (R_aeq* v0) R_aeq). cut (SN S v0). 2:{ apply wf_restrict_sn. intros v hv. eapply proper_atc. class. 2: apply hv. class. apply P_sn. hyp. } apply SN_ind; intros v i IH v0v. apply Q_neu. destruct t_neu_or_abs as [t_neu|[x [u e]]]. apply neutral_app. hyp. rewrite e. apply neutral_beta. intros w tv_w. inversion tv_w as [? a ? w' tv_a ww' aw']; clear tv_w; subst. inv_aeq tv_a; clear tv_a; subst; rename u into t'; rename u0 into v'. inversion aw'; clear aw'; subst. destruct t_neu_or_abs as [t_neu|[x [u e]]]. exfalso. eapply not_Rh_app_neutral. 2: apply H. rewrite i1. hyp. rewrite e in i1. inv_aeq i1; clear i1. rewrite i0 in H. apply Rh_bh in H. inversion H; clear H; subst x1 u1 v1 w'. rewrite ww', i3, single_rename. rewrite fold_subs_single, i2. eapply proper_atc. hyp. apply Q_red. eapply subs_single_mon_preorder_aeq; class. apply v0v. refl. apply tv0_beta_comp. hyp. tauto. rewrite ww'. apply t_red_comp. rewrite <- i1. apply clos_aeq_intro_refl. hyp. rewrite i2. gen (proper_atc P_aeq P_red); intro P_reds. assert (h : Proper (Logic.eq ==> R_aeq* ==> aeq ==> R_aeq*) subs_single). apply subs_single_mon_preorder_aeq; class. rewrite <- v0v. hyp. rewrite ww', i1. apply IH. split. hyp. rewrite <- i2. apply clos_aeq_intro_refl. hyp. trans v. hyp. rewrite <- i2. apply at_step. apply clos_aeq_intro_refl. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)