proposition: Theorem eval_inductive_prop : forall A B (P : A -> B -> Prop) (opsA : operations A) (opsB : operations B), (forall o a b, P a b -> P (unary opsA o a) (unary opsB o b)) -> (forall o a1 a2 b1 b2, P a1 b1 -> P a2 b2 -> P (binary opsA o a1 a2) (binary opsB o b1 b2)) -> forall inpA inpB, (forall n, P (nth n inpA (unknown opsA)) (nth n inpB (unknown opsB))) -> forall prog, forall n, P (nth n (eval_generic opsA prog inpA) (unknown opsA)) (nth n (eval_generic opsB prog inpB) (unknown opsB)).
proof: Proof. intros A B P opsA opsB Hun Hbin inpA inpB Hinp prog. do 2 rewrite rev_formula. induction (rev prog). exact Hinp. intros [|n]. 2: apply IHl. destruct a as [n|o n|o n1 n2] ; [ idtac | apply Hun | apply Hbin ] ; apply IHl. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree