proposition: Lemma uni_normalise_correct I: U X I <-> U X (uni_normalise I).
proof: Proof. split; intros H; [eapply @U_reduction|eapply @U_reduction with (I := uni_normalise I)]. all: trivial; cbn; eapply equiv_join. 1, 3, 6, 8: rewrite eta_correct. all: reflexivity. Qed.
imports: List Lia Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order evaluator)