proposition: Lemma Formula_depth_rec_indep : forall (Q P : Formula -> Set) (rec : forall a : Formula, (forall b : Formula, lt_depth b a -> Q b -> P b) -> Q a -> P a), (forall (a : Formula) (z1 z2 : forall b : Formula, lt_depth b a -> Q b -> P b), (forall (b : Formula) (p : lt_depth b a) (q : Q b), z1 b p q = z2 b p q) -> forall q : Q a, rec a z1 q = rec a z2 q) -> forall (a : Formula) (q : Q a), Formula_depth_rec (fun x : Formula => Q x -> P x) rec a q = rec a (fun (b : Formula) _ => Formula_depth_rec (fun x : Formula => Q x -> P x) rec b) q.
proof: Proof. intros Q P rec H. unfold Formula_depth_rec in |- *. set (H0 := Formula_depth_rec_rec (fun x : Formula => Q x -> P x) rec) in *. assert (H1: forall (n m : nat) (b : Formula) (l1 : depth b <= n) (l2 : depth b <= m) (q : Q b), H0 n b l1 q = H0 m b l2 q). { simple induction n. - simpl in |- *. intros m b l1 l2 q; induction m as [| m Hrecm]. + simpl in |- *; apply H. intros b0 p q0. induction (Nat.nlt_0_r (depth b0) (eq_ind_r (fun n0 : nat => depth b0 < n0) p (Compat815.le_n_0_eq (depth b) l1))). + intros; simpl ; apply H. intros b0 p q0. induction (Nat.nlt_0_r (depth b0) (eq_ind_r (fun n0 : nat => depth b0 < n0) p (Compat815.le_n_0_eq (depth b) l1))). - simple induction m. + intros b l1 l2 q; simpl in |- *; apply H. intros b0 p q0. induction (Nat.nlt_0_r (depth b0) (eq_ind_r (fun n1 : nat => depth b0 < n1) p (Compat815.le_n_0_eq (depth b) l2))). + intros n1 H2 b l1 l2 q; simpl in |- *; apply H. intros b0 p q0. apply H1. } intros a q; replace (H0 (depth a) a (le_n (depth a)) q) with (H0 (S (depth a)) a (Nat.le_succ_diag_r (depth a)) q). - simpl in |- *; apply H. intros; apply H1. - apply H1. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )