proposition: Lemma lift_bin_rel_if : forall {T:[univ]} (R : bin_rel T) (b:bool) nl1 nl2 nr1 nr2, R nl1 nr1 -> R nl2 nr2 -> R (if b then nl1 else nl2) (if b then nr1 else nr2).
proof: Proof. intros. cases_if; sp. Qed.
imports: UsefulTypes