From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 16 Oct 2008 17:16:58 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4678
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=237ade59af59ffa7c4a754407b1f55e057be4208;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index 4bfe88a8b..fd1cc9057 100644
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -10,7 +10,7 @@ inductive Formula : Type ≝
 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
 .
 
-let rec sem (v: nat -> nat) (F: formula) on F ≝
+let rec sem (v: nat -> nat) (F: Formula) on F ≝
  match F with
   [ FBot ⇒ 0
   | FTop ⇒ (*BEGIN*)1(*END*)
@@ -37,7 +37,7 @@ for @{ 'if_then_else $e $t $f }.
 
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else e t f).
 
-let rec subst (x:nat) (G: Formula) (F: formula) on F ≝
+let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
  match F with
   [ FBot ⇒ FBot
   | FTop ⇒ (*BEGIN*)FTop(*END*)
@@ -68,7 +68,7 @@ assume F2 : Formula.
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).
-assume H : (F1 ≡_v F2).
+suppose (F1 ≡_v F2) (H).
 we proceed by induction on F to prove (subst x F1 F ≡_v subst x F2 F). 
 case Bot.
   the thesis becomes (FBot ≡_v (subst x F2 FBot)).