]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2A/grammar/tsts_tsts.ma
update in binararies for λδ
[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / grammar / tsts_tsts.ma
index 50f8291713d33ad89540b2432dbfc3ef74c16f1d..7f4a31da60bf73f3251643553175f030e1218342 100644 (file)
@@ -18,7 +18,6 @@ include "basic_2A/grammar/tsts.ma".
 
 (* Main properties **********************************************************)
 
-(* Basic_1: was: iso_trans *)
 theorem tsts_trans: Transitive … tsts.
 #T1 #T * -T1 -T //
 #I #V1 #V #T1 #T #X #H