proposition: Lemma F_inj' n m : F n = F m -> ~ n < m.
proof: Proof. intros H1 H2 % F_lt. rewrite H1 in H2. apply (F_nel H2). Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia