X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Futil.ma;h=3521e87ddf7ee1abde19af4ea3154e7003d8adf9;hb=aba1baf85bb8e6b3ea3e66a8c2d07601066d26bc;hp=bd7018d3c4488bc03aa3cfbeac5e459b09650035;hpb=bfb7fbf61e86114e49cb3671503e8307a4582342;p=helm.git diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma index bd7018d3c..3521e87dd 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Fsub/util". include "logic/equality.ma". include "nat/compare.ma". include "list/list.ma". @@ -55,4 +54,4 @@ lemma max_case : \forall m,n.(max m n) = match (leb m n) with [ true \Rightarrow n | false \Rightarrow m ]. intros;elim m;simplify;reflexivity; -qed. \ No newline at end of file +qed.