proposition: Lemma reduction_transitive P Q R: P ⪯ Q -> Q ⪯ R -> P ⪯ R.
proof: Proof. intros [f H1] [g H2]; exists (f >> g). intros x; rewrite H1, H2. reflexivity. Qed.
imports: Lia List Undecidability.HOU(std.lists.basics std.misc std.decidable)