proposition: Lemma R_right_app_monotonous : forall M N M' N' (M'app: isApp M') (N'app: isApp N'), algebraic M -> M -R-> N -> appBodyL M'app = M -> appBodyL N'app = N -> appBodyR M'app = appBodyR N'app -> algebraic (appBodyR M'app) -> M' -R-> N'.
proof: Proof. intros. term_inv M'; term_inv N'. try (rename A0 into A1; rename A into A0). assert (EE0: E = E0). replace E with (env M). replace E0 with (env N). apply R_env_preserving; trivial. rewrite <- H2; trivial. rewrite <- H1; trivial. set (Lpos := PAppL T2 (PThis (buildT T1))). assert (W: {P: PlaceHolder Lpos | proj1_sig2 P = M}). assert (env (buildT (TApp T1 T2) // Lpos) = env M). rewrite <- H1; trivial. assert (type (buildT (TApp T1 T2) // Lpos) = type M). rewrite <- H1; trivial. exists (exist2 (fun T => env (buildT (TApp T1 T2) // Lpos) = env T) (fun T => type (buildT (TApp T1 T2) // Lpos) = type T) M H5 H6 ); trivial. assert (W': {P: PlaceHolder Lpos | proj1_sig2 P = N}). assert (env (buildT (TApp T1 T2) // Lpos) = env N). rewrite <- H2; trivial. assert (type (buildT (TApp T1 T2) // Lpos) = type N). simpl. replace (A0 --> B) with (type M). apply R_type_preserving; trivial. rewrite <- H1; trivial. exists (exist2 (fun T => env (buildT (TApp T1 T2) // Lpos) = env T) (fun T => type (buildT (TApp T1 T2) // Lpos) = type T) N H5 H6 ); trivial. replace Tr with (swap (proj1_sig W)); destruct W; simpl in * . replace Tr0 with (swap (proj1_sig W')); destruct W'; simpl in * . apply R_monotonous; simpl; trivial. apply algebraic_app with I; trivial. simpl; rewrite H1; trivial. rewrite e; trivial. rewrite e0; trivial. apply R_algebraic_preserving with M; trivial. apply algebraic_arrowType; trivial. rewrite H1; trivial. rewrite e, e0; trivial. apply term_eq. rewrite swap_env_eq; trivial. rewrite swap_term_is; simpl; trivial. rewrite e0, <- H2; simpl. change PtR with (term (buildT T2)). rewrite H3; trivial. apply term_eq. rewrite swap_env_eq; trivial. rewrite swap_term_is; simpl; trivial. rewrite e, <- H1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)