proposition: Lemma lift_bin_rel_ifdp : forall {T:[univ]} {Pl Pr : Prop} (R : bin_rel T) (b: (@sumbool Pl Pr)) 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