1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / bool_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
index a837712532b655071995e3f24133e367f9432a67..2ae4388886a849b425cd2ed041862d22f8c24d94 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -59,7 +59,7 @@ nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
  nelim b1;
  nelim b2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_andbool : symmetricT bool bool and_bool.
@@ -67,7 +67,7 @@ nlemma symmetric_andbool : symmetricT bool bool and_bool.
  nelim b1;
  nelim b2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
@@ -76,7 +76,7 @@ nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗
  nelim b2;
  nelim b3;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_orbool : symmetricT bool bool or_bool.
@@ -84,7 +84,7 @@ nlemma symmetric_orbool : symmetricT bool bool or_bool.
  nelim b1;
  nelim b2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
@@ -93,7 +93,7 @@ nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b
  nelim b2;
  nelim b3;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
@@ -101,7 +101,7 @@ nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
  nelim b1;
  nelim b2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
@@ -110,7 +110,7 @@ nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙
  nelim b2;
  nelim b3;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
@@ -118,8 +118,8 @@ nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,4: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -128,8 +128,8 @@ nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,4: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -138,8 +138,8 @@ nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,2: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,2: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -148,8 +148,8 @@ nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,3: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,3: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -158,8 +158,8 @@ nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##4: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -168,7 +168,7 @@ nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##4: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.