]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
- improved Makefile esp. with the "trim" function
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv_ltpr.ma
index c17f7e071f1bb650b4a86ed4bcecf82a3c9665ce..ba47b1e47d5bbecc5a21ebed16f77f7fd3638b6a 100644 (file)
@@ -74,4 +74,4 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
     elim (IH3 … HVW1 … HL12 … HV12) // [2: /2 width=1/ ] -HV1 -HVW1 -HV12 #W200 #HVW200 #H
     lapply (cpcs_trans … HW210 … H) -W10 #HW200
     lapply (lsubsv_snv_trans … HT2 (L2.ⓓV2) ?) -L1 -HT2 /2 width=1/ /2 width=4/
-  | 
\ No newline at end of file
+  |
\ No newline at end of file