proposition: Lemma rule_1 : buildT t_1_l >> buildT t_1_r.
proof: Proof. constructor; try_solve. 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. rewrite <- M'eq. apply AlgVar. try_solve. apply AlgFunApp; try_solve. compute. trivial. apply HSub. compute. trivial. exists (@appBodyR (@appBodyL (buildT t_1_l) I) I). left. trivial. right. Qed.
imports: CoLoR(TermsSig Horpo HorpoWf RelExtras Terms LogicUtil) Coq(List Wf_nat)