proposition: Theorem rel_subset : forall x xr : R, forall xi zi : FF, REL x xr xi -> rel_subset_helper xi zi = true -> REL x xr zi.
proof: Proof. intros x xr xi zi (xe,(Hx1,Hx2)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). apply Fle2_correct in H1. apply Fle2_correct in H2. exists xe. split. apply IRsubset with (1 := H1) (2 := H2) (3 := Hx1). exact Hx2. Qed.
imports: Gappa_common Gappa_pred_bnd