...

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index 4bfe88a8bfea2743bd7bf40191298125387ca3eb..fd1cc90576a90fa36e9f10773cc25fdb1b7a26d0 100644 (file)
--- 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)).