]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma
partial commit: "computation" component ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lpxs_lpxs.ma
index d9a152db90bc4c8f1675f28e5cc131cef20e8635..998f89e144e835a5eb755e73a3142f78a0757a89 100644 (file)
@@ -18,5 +18,5 @@ include "basic_2/computation/lpxs.ma".
 
 (* Main properties **********************************************************)
 
-theorem lpxs_trans: ∀h,g. Transitive … (lpxs h g).
+theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G).
 /2 width=3/ qed-.