commit by user mkmluser

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / basic_1.txt

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index 544232544fbe7a7bfafc5db1005da0365e3738c1..c5fe6def0932a2c8fcf2db186caa9c28cdca7b8f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -209,9 +209,7 @@ ty3/arity ty3_arity
 ty3/arity_props ty3_predicative
 ty3/arity_props ty3_repellent
 ty3/arity_props ty3_acyclic
-ty3/arity_props ty3_sn3
 ty3/dec ty3_inference
-ty3/fwd ty3_gen_appl
 ty3/fwd tys3_gen_nil
 ty3/fwd tys3_gen_cons
 ty3/fwd_nf2 ty3_gen_appl_nf2