proposition: Lemma monotonicity_criterion : (forall M M' (Mapp: isApp M) (M'app: isApp M'), appBodyL Mapp -R-> appBodyL M'app -> appBodyR Mapp = appBodyR M'app -> M -R-> M' ) -> (forall M M' (Mapp: isApp M) (M'app: isApp M'), appBodyL Mapp = appBodyL M'app -> appBodyR Mapp -R-> appBodyR M'app -> M -R-> M' ) -> (forall N N' (Nabs: isAbs N) (N'abs: isAbs N'), absType Nabs = absType N'abs -> absBody Nabs -R-> absBody N'abs -> N -R-> N' ) -> monotonous.
proof: Proof. unfold monotonous; intros M_AppL M_AppR M_Abs. induction pos; simpl; intros Mpos Npos MN. replace (swap Mpos) with (proj1_sig2 Mpos). replace (swap Npos) with (proj1_sig2 Npos). trivial. apply term_eq. rewrite swap_env_eq; destruct Npos; try_solve. rewrite swap_term_is; try_solve. apply term_eq. rewrite swap_env_eq; destruct Mpos; try_solve. rewrite swap_term_is; try_solve. set (Labs := swap_abs Mpos). set (Rabs := swap_abs Npos). apply M_Abs with Labs Rabs. apply type_eq_absType_eq. do 2 rewrite swap_type_eq; trivial. destruct (placeHolder_abs Mpos) as [MLpos ML]. destruct (placeHolder_abs Npos) as [NLpos NL]. replace (absBody Labs) with (swap MLpos). replace (absBody Rabs) with (swap NLpos). apply IHpos. rewrite ML; rewrite NL; trivial. apply swap_in_abs; trivial. apply TAbs; trivial. apply swap_in_abs; trivial. apply TAbs; trivial. set (Lapp := swap_left_app Mpos). set (Rapp := swap_left_app Npos). apply M_AppL with Lapp Rapp. destruct (placeHolder_appL Mpos) as [MLpos ML]. destruct (placeHolder_appL Npos) as [NLpos NL]. replace (appBodyL Lapp) with (swap MLpos). replace (appBodyL Rapp) with (swap NLpos). apply IHpos. rewrite ML; rewrite NL; trivial. apply swap_in_appL; trivial. apply swap_in_appL; trivial. apply swap_appR_eq. set (Lapp := swap_right_app Mpos). set (Rapp := swap_right_app Npos). apply M_AppR with Lapp Rapp. apply swap_appL_eq. destruct (placeHolder_appR Mpos) as [MLpos ML]. destruct (placeHolder_appR Npos) as [NLpos NL]. replace (appBodyR Lapp) with (swap MLpos). replace (appBodyR Rapp) with (swap NLpos). apply IHpos. rewrite ML; rewrite NL; trivial. apply swap_in_appR; trivial. apply swap_in_appR; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)