]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma
partial commit: just the components before "static" ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / csn_aaa.ma
index cd8d5a64b7ef7df7aeb11c29221b6734db04597f..f5229400f74d98e83277f556afa55a5e2f9eb0ac 100644 (file)
@@ -19,7 +19,7 @@ include "basic_2/computation/csn_tstc_vector.ma".
 
 (* Main properties concerning atomic arity assignment ***********************)
 
-theorem csn_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ⦃h, L⦄ ⊢ ⬊*[g] T.
+theorem csn_aaa: ∀h,g,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
 #h #g #L #T #A #H
 @(acp_aaa … (csn_acp h g) (csn_acr h g) … H)
 qed.