proposition: Lemma horpo_not_trans : ~transitive horpo.
proof: Proof. assert (algebraic (buildT t1)). apply AlgApp; try_solve. intros. destruct H as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgAbs with I. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H as [M''eq | false]; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgFunApp; try_solve. compute. trivial. assert (algebraic (buildT t2)). apply AlgApp; try_solve. intros. destruct H0 as [M'eq | [M'eq | false]]; try_solve. rewrite <- M'eq. apply AlgAbs with I. apply AlgFunApp; try_solve. compute. trivial. intros. destruct H0 as [M''eq | false]; try_solve. rewrite <- M''eq. apply AlgVar; try_solve. rewrite <- M'eq. apply AlgFunApp; try_solve. compute. trivial. assert (algebraic (buildT t3)). apply AlgFunApp; try_solve. compute. trivial. intros. destruct H1 as [M'eq | false]; try_solve. rewrite <- M'eq. apply AlgFunApp; try_solve. compute. trivial. intro Htr. absurd (buildT t1 >> buildT t3). intro t1t3. inversion t1t3. inversion H6; try_solve. inversion H9; try_solve. inversion H12. absurd (term (lower (subst (beta_subst (buildT t1) Mapp0 MLabs)) (beta_lowering (buildT t1) Mapp0 MLabs)) = term (buildT t3)). rewrite lower_term, subst_term. discr. rewrite <- H17. trivial. apply (Htr (buildT t1) (buildT t2) (buildT t3)). assert (@appBodyR (buildT t1) I >> @appBodyR (buildT t2) I). constructor; try solve [try_solve | apply AlgFunApp; compute; tauto]. apply HFun with a b; compute; trivial. apply HArgsNil. apply horpo_app_inv with I I. repeat split; intuition. hyp. intuition. hyp. repeat split. right. left. hyp. right. hyp. constructor; try_solve. apply HBeta. apply RedStep. replace (buildT t3) with (lower (subst (beta_subst (buildT t2) I I)) (beta_lowering (buildT t2) I I)). apply Beta. apply term_eq. rewrite lower_env, subst_env. trivial. rewrite lower_term, subst_term. trivial. Qed.
imports: CoLoR(TermsSig Horpo HorpoWf RelExtras Terms LogicUtil) Coq(Wf_nat List)