Remove extraneous hypotheses

leanprover-community · Nov 26, 2024 · fa12670 · fa12670
1 parent 214c408
commit fa12670
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/ConNF/Construction/RunInduction.lean b/ConNF/Construction/RunInduction.lean
@@ -18,8 +18,7 @@ open Cardinal Ordinal WithBot
 
 namespace ConNF
 
-variable [Params.{u}] {α : Λ} (M : (β : Λ) → (β : TypeIndex) < α → Motive β)
-  (H : (β : Λ) → (h : (β : TypeIndex) < α) → Hypothesis (M β h) λ γ h' ↦ M γ (h'.trans h))
+variable [Params.{u}]
 
 instance : IsTrans Λ λ β γ ↦ (β : TypeIndex) < (γ : TypeIndex) :=
   ⟨λ _ _ _ ↦ lt_trans⟩