- new extendedd beta-reductum involving native type annotation

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / csn_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
index 21d97b7746b627f73cb26904b94025a837bbd7ad..e57f37d9da00f3e886f832a0fbe8c258602a16d0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
@@ -96,5 +96,6 @@ theorem csn_acp: ∀h,g. acp (cpx h g) (eq …) (csn h g).
   #l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/
 | @cnx_lift
 | /2 width=3 by csn_fwd_flat_dx/
+| /2 width=1/
 ]
 qed.