proposition: Lemma pow_trans_eq: forall (s t u : term) (i j k: nat), s >(i) t -> t >(j) u -> i+j=k -> s >(k) u.
proof: Proof. intros. subst. eapply pow_trans;eauto. Qed.
imports: Undecidability.L(Util.L_facts) ListTactics Undecidability.L.Tactics(Lproc Reflection)