proposition: Lemma eq_true_inj (b b' : bool) : is_true b = is_true b' -> b = b'.
proof: Proof. intro. induction b; induction b'. reflexivity. unfold is_true in H. symmetry. rewrite <- H. reflexivity. unfold is_true in H. rewrite H; reflexivity. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii