]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
- degree assignment, static type assignment, iterated static type
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cpxs_tstc_vector.ma
index cf9b76f293a5345b2935a6ee5e040a891b576e79..cea820cfbc4aa4e29585cce2529f33f0d7188848 100644 (file)
@@ -185,7 +185,7 @@ elim (cpxs_inv_appl1 … H) -H *
     @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /2 width=3/
   | @or3_intro2 -T (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -W /2 width=3/  
+    @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -W /2 width=3/
   ]
 ]
 qed-.