proposition: Lemma monotonous_appL : forall M N (Mapp: isApp M) (Napp: isApp N), appBodyL Mapp -R-> appBodyL Napp -> appBodyR Mapp = appBodyR Napp -> M -R-> N.
proof: Proof. intros M N Mapp Napp MNl MNr. set (pos := posAppLeft M Mapp). assert (envOkL: env (M // pos) = env (appBodyL Mapp)). term_inv M. assert (typeOkL: type (M // pos) = type (appBodyL Mapp)). term_inv M. set (Tl := exist2 (fun L => env (M // pos) = env L) (fun L => type (M // pos) = type L) (appBodyL Mapp) envOkL typeOkL). assert (envOkR: env (M // pos) = env (appBodyL Napp)). apply R_env_preserving; term_inv M. assert (typeOkR: type (M // pos) = type (appBodyL Napp)). apply R_type_preserving; term_inv M. set (Tr := exist2 (fun R => env (M // pos) = env R) (fun R => type (M // pos) = type R) (appBodyL Napp) envOkR typeOkR). replace M with (swap Tl). replace N with (swap Tr). apply R_monotonous; trivial. apply term_eq. rewrite swap_env_eq; term_inv M; term_inv N. rewrite swap_term_is; term_inv M; term_inv N. change PtR with (term (buildT T2)). rewrite MNr; trivial. apply term_eq. rewrite swap_env_eq; term_inv M; term_inv N. rewrite swap_term_is; term_inv M; term_inv N. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)