proposition: Lemma If_eq_simple : forall P P' x x' y y', (P <-> P') -> (x = x') -> (y = y') -> (If P then x else y) = (If P' then x' else y').
proof: Proof. Proof using. intros. subst. asserts_rewrite (P = P'). apply~ prop_ext. auto. Qed.
imports: TLC(LibTactics)