proposition: Lemma RSR_h_PropEx : forall P : IR -> Prop, pred_wd' IR P -> {i : nat | {Hi : _ < _ | P (f' i Hi)}} or {j : nat | {Hj : _ < _ | P (g' j Hj)}} -> {k : nat | {Hk : _ < _ | P (h k Hk)}}.
proof: Proof. unfold h in |- *; intros; apply om_fun_4d; auto. exact RSR_f'_nlnf. exact RSR_g'_nlnf. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)