proposition: Lemma RSR_h_PropAll : forall P : IR -> Prop, pred_wd' IR P -> (forall (i : nat) Hi, P (f' i Hi)) -> (forall (j : nat) Hj, P (g' j Hj)) -> forall (k : nat) Hk, P (h k Hk).
proof: Proof. unfold h in |- *; apply om_fun_4b. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)