]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma
- fpbg can be reflexive (example given)
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv_scpes.ma
index 2c3a1d35c66f293d207024bb8a9341e9e863b876..4895a510577686bea0ff7c9ae4c3299aa634e8fc 100644 (file)
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/fpbs_lift.ma".
-include "basic_2/computation/fpbg_fleq.ma".
+include "basic_2/computation/fpbg_fpbs.ma".
 include "basic_2/equivalence/scpes_cpcs.ma".
 include "basic_2/equivalence/scpes_scpes.ma".
 include "basic_2/dynamic/snv.ma".