proposition: Lemma If_eq : forall P P' x x' y y', (P <-> P') -> (P -> x = x') -> (~P -> y = y') -> (If P then x else y) = (If P' then x' else y').
proof: Proof. Proof using. intros. do 2 case_if; autos*. Qed.
imports: TLC(LibTactics)