proposition: Lemma om_fun_4b : forall n m f g Hfg (P : F -> Prop), pred_wd' F P -> (forall i Hi, P (f i Hi)) -> (forall j Hj, P (g j Hj)) -> forall k Hk, P (om_fun n m f g Hfg k Hk).
proof: Proof. intro n. induction n as [| n Hrecn]. simpl in |- *; auto. intro m; induction m as [| m Hrecm]. simpl in |- *; auto. intros. simpl in |- *; elim ap_imp_less; simpl in |- *; intro; elim le_lt_eq_dec; simpl in |- *; intro; auto. set (h := fun i Hi => g i (Nat.lt_lt_succ_r _ _ Hi)) in *. set (Hfh := fun i j Hi Hj => Hfg i j Hi (Nat.lt_lt_succ_r _ _ Hj)) in *. set (Hh := fun i Hi => H1 i (Nat.lt_lt_succ_r _ _ Hi)) in *. exact (Hrecm f h Hfh P H H0 Hh k (om_fun_lt _ _ a0)). apply Hrecn; auto. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)