X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fduality.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fduality.ma;h=28e254f9477726bdcc9fc84e717b74add40d6557;hb=7cb22a7f8107a6cde0b77b7879e04f586a347102;hp=aa1aa32f8859e4602b8c8eb186ab7968cdb699a7;hpb=cb25e0f32f7581e1a49d1d1c109108763dfb882c;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma
index aa1aa32f8..28e254f94 100644
--- a/helm/software/matita/library/didactic/exercises/duality.ma
+++ b/helm/software/matita/library/didactic/exercises/duality.ma
@@ -220,7 +220,7 @@ definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
-lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed.
+lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
 
 (* Esercizio 3
    ===========