proposition: Lemma bool_equiv_true: forall (f g: bool), (f = true <-> g = true) <-> (f = g).
proof: Proof. intros f g; destruct f, g; intuition. Qed.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Bool.Bool Coq.Classes.Morphisms Fiat.Common.Coq__8_4__8_5__Compat