proposition: Remark Formula_depth_rec2rec_nice : forall (Q P : Formula -> Set) (f1 : forall t t0 : Term, Q (equal t t0) -> P (equal t t0)) (f2 : forall (r : Relations L) (t : Terms (arityR L r)), Q (atomic r t) -> P (atomic r t)) (f3 : forall f : Formula, (Q f -> P f) -> forall f0 : Formula, (Q f0 -> P f0) -> Q (impH f f0) -> P (impH f f0)), (forall (f g : Formula) (z1 z2 : Q f -> P f), (forall q : Q f, z1 q = z2 q) -> forall z3 z4 : Q g -> P g, (forall q : Q g, z3 q = z4 q) -> forall q : Q (impH f g), f3 f z1 g z3 q = f3 f z2 g z4 q) -> forall f4 : forall f : Formula, (Q f -> P f) -> Q (notH f) -> P (notH f), (forall (f : Formula) (z1 z2 : Q f -> P f), (forall q : Q f, z1 q = z2 q) -> forall q : Q (notH f), f4 f z1 q = f4 f z2 q) -> forall f5 : forall (v : nat) (a : Formula), (forall b : Formula, lt_depth b (forallH v a) -> Q b -> P b) -> Q (forallH v a) -> P (forallH v a), (forall (v : nat) (a : Formula) (z1 z2 : forall b : Formula, lt_depth b (forallH v a) -> Q b -> P b), (forall (b : Formula) (q : lt_depth b (forallH v a)) (r : Q b), z1 b q r = z2 b q r) -> forall q : Q (forallH v a), f5 v a z1 q = f5 v a z2 q) -> 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, Formula_depth_rec2rec (fun x : Formula => Q x -> P x) f1 f2 f3 f4 f5 a z1 q = Formula_depth_rec2rec (fun x : Formula => Q x -> P x) f1 f2 f3 f4 f5 a z2 q.
proof: Proof. intros Q P f1 f2 f3 H f4 H0 f5 H1 a z1 z2 H2 q. induction a as [t t0| r t| a1 Hreca1 a0 Hreca0| a Hreca| n a Hreca]. - auto. - auto. - simpl in |- *; apply H. + intros q0; apply H2. + intros q0; apply H2. - simpl in |- *; apply H0; intros q0; apply H2. - simpl in |- *; apply H1, H2. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )