proposition: Lemma isTrue_eq_isTrue_eq : forall P1 P2, (isTrue P1 = isTrue P2) = (P1 <-> P2).
proof: Proof. Proof using. intros. extens. iff; repeat rewrite isTrue_eq_if in *; repeat case_if; auto_false*. Qed.
imports: TLC(LibTactics)