proposition: Lemma isTrue_If_eq_if_isTrue : forall P1 P2 P3, isTrue (If P1 then P2 else P3) = (if isTrue P1 then isTrue P2 else isTrue P3).
proof: Proof. Proof using. intros. rewrite if_isTrue. rewrite~ isTrue_If. Qed.
imports: TLC(LibTactics)