Commit 35a678eb authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

raccourci : lazy_andb_iff au lieu de andb_lazy_alt + andb_true_iff

parent 4728e3c7
......@@ -1382,7 +1382,7 @@ Proof.
- rewrite <- Names.is_empty_spec. namedec.
- rewrite <- Names.is_empty_spec. namedec.
- apply (term_fclosed_spec (Fun "" l)).
- rewrite <- andb_lazy_alt, andb_true_iff, IHf1, IHf2.
- rewrite lazy_andb_iff, IHf1, IHf2.
intuition.
Qed.
......
......@@ -208,7 +208,7 @@ Proof.
{ induction t as [ | | f l IH] using term_ind'; cbn; trivial.
- unfold BogusPoint. now rewrite <- SO.
- destruct (funsymbs sign f) as [ar|] eqn:E; try easy.
rewrite <- andb_lazy_alt, andb_true_iff. intros (_ & F) genv lenv.
rewrite lazy_andb_iff. intros (_ & F) genv lenv.
destruct (FU f) as [Hf|Hf].
+ exfalso. now rewrite (funsOk mo f), Hf in E.
+ rewrite <- Hf. destruct (funs mo f) as [(p,q)|]; auto.
......@@ -219,12 +219,12 @@ Proof.
- intuition.
- intuition.
- destruct (predsymbs sign p) as [ar|] eqn:E; try easy.
rewrite <- andb_lazy_alt, andb_true_iff. intros (_ & F) genv lenv.
rewrite lazy_andb_iff. intros (_ & F) genv lenv.
rewrite <- PR. destruct (preds mo p) as [(u,v)|]; try easy.
f_equiv. apply map_ext_in. intros a Ha. apply Ht.
rewrite forallb_forall in F; auto.
- intros WA genv lenv. now rewrite IHA.
- rewrite <- andb_lazy_alt, andb_true_iff.
- rewrite lazy_andb_iff.
intros (WA1,WA2) genv lenv.
specialize (IHA1 WA1 genv lenv).
specialize (IHA2 WA2 genv lenv).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment