]> matita.cs.unibo.it Git - helm.git/commitdiff
;auto fixed
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 6 Jan 2007 16:14:06 +0000 (16:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 6 Jan 2007 16:14:06 +0000 (16:14 +0000)
matita/contribs/RELATIONAL/NLE/fwd.ma
matita/contribs/RELATIONAL/NLE/props.ma

index 5ddeb41aff1b1efe28b47c639310f49cd8373f50..afefbfd4db919ed53eea720b2dc927d4047555e0 100644 (file)
@@ -25,7 +25,7 @@ theorem nle_gen_succ_1: \forall x,y. x < y \to
  intros. decompose.
  lapply linear nplus_gen_succ_2 to H1 as H.
  decompose. subst.
- apply ex_intro; auto. (**)
+ apply ex_intro;[| auto] (**)
 qed.
 
 
index b571dfc6b46f9e8ab9385bef2462baf354e1d286..549eae418c2762cca71c10f6e8de7a706ba87719 100644 (file)
@@ -24,7 +24,7 @@ qed.
 theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q.
  unfold NLE.
  intros. decompose.
- apply ex_intro; auto. (**)
+ apply ex_intro; [|auto] (**)
 qed.
 
 theorem nle_refl: \forall x. x <= x.