proposition: Lemma ord_target' Gamma: ord' (target' Gamma) <= 1.
proof: Proof. eapply ord'_elements; unfold target'; intros; mapinj; eauto using ord_target. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)