proposition: Lemma if_isTrue : forall P A (x y : A), (if isTrue P then x else y) = (If P then x else y).
proof: Proof. Proof using. intros. case_if as C; case_if as D; auto. { rewrite* isTrue_eq_true_eq in C. } { rewrite* isTrue_eq_false_eq in C. } Qed.
imports: TLC(LibTactics)