proposition: Lemma enum_3N_stupid: (fun e => True) |= enum_3N {= fun e => False =}.
proof: Proof. apply PHL.soundness. simpl. constructor 1 with (x:=fun _:Env => True). intuition (discriminate || auto). Qed.
imports: ZArith Znumtheory hoarelogic Zwf Wellfounded Lia