X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Ffwd.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Ffwd.ma;h=518bb5ff064f169a3128a6d89ad55521c865d2c8;hb=1994fe8e6355243652770f53a02db5fdf26915f0;hp=8738e723477753937d43b49254e1449b438b7f0d;hpb=78d9265b6261eb24cad483fb57a386e39eae6a3c;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma index 8738e7234..518bb5ff0 100644 --- a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma +++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma @@ -90,5 +90,5 @@ let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to Prop)) (f: (\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall (y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a \def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y: -A).(\lambda (r: (R y x)).((Acc_ind A R P f) y (a1 y r)))))]. +A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))].