proposition: Theorem bnd_of_bnd_rel_o : forall x y : R, forall yi ei xi : FF, BND y yi -> REL x y ei -> mul_op_helper yi (one_plus ei) xi = true -> BND x xi.
proof: Proof. intros x y yi ei xi Hy (e,(He1,He2)) Hb. rewrite He2. apply mul_op with (1 := Hy) (3 := Hb). apply one_plus_correct with (1 := He1). Qed.
imports: Gappa_common Gappa_pred_bnd