proposition: Lemma rule_2 : buildT t_2_l >> buildT t_2_r.
proof: Proof. assert (t2alg: algebraic (buildT t_2_l)). apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M''eq | [M''eq | false]]; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. constructor; try_solve. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgApp; try_solve. intros. destruct H as [M''eq | [M''eq | false]]; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M''eq | [M''eq | false]]; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. apply HFun with map cons; try_solve. compute. apply HArgsConsEqT. constructor; try_solve. apply AlgApp; try_solve. intros. destruct H as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. match goal with | |- _ >-> buildT (TApp ?X ?Y) => set (Vx := buildT X); set (Vy := buildT Y) end. apply HAppFlat with (Vx :: Vy :: List.nil); try_solve. compute. trivial. apply HArgsConsNotEqT. exists (@appBodyR (buildT t_2_l) I). apply appArg_right with I. trivial. right. apply HArgsConsNotEqT. exists (@appBodyR (@appBodyL (buildT t_2_l) I) I). left. trivial. left. constructor; try_solve. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. apply AlgVar. try_solve. apply HSub. compute. trivial. eexists (buildT (@TVar env_2 0 #(Star) _)). compute. left. trivial. constructor 2. apply HArgsNil. apply HArgsConsEqT. constructor; try_solve. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. match goal with | |- ?L >-> ?R => set (TL := L); set (TR := R) end. assert (@appBodyR (@appBodyL TL I) I >> @appBodyR (@appBodyL TR I) I). constructor; try_solve. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgVar; try_solve. apply AlgVar; try_solve. apply HSub. compute. trivial. match goal with | |- exists2 _, isArg _ ?T & _ => exists (@appBodyR T I) end. right. left. trivial. right. apply HMul with map; try_solve. constructor. set (w := pair_mOrd_fromList). unfold MSet.list2multiset in w. apply w. apply horpo_eq_compat'. left. hyp. right. compute. trivial. left. hyp. apply HArgsNil. Qed.
imports: CoLoR(TermsSig Horpo HorpoWf RelExtras Terms LogicUtil) Coq(List Wf_nat)