clean up def extension_of_isomorphism

vaibhavkarve · Mar 12, 2021 · 0762b9d · 0762b9d
1 parent 93772b0
commit 0762b9d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/model.lean b/src/model.lean
@@ -845,8 +845,8 @@ def extend_struc_by_element : sorry := sorry
 
 
 def extension_of_isomorphism (t : theory L) (M₁ M₂ : Model t) :
-  ∀ (S₁ : substruc M₁.M) (S₂ : substruc M₂.M) [fin_substruc S₁] [fin_substruc S₂]
-  (η : isomorphism S₁ S₂),
+  ∀ (S₁ : substruc M₁.M) (S₂ : substruc M₂.M) [fin_substruc S₁] [fin_substruc S₂],
+  ∀ (η : @isomorphism L ↑S₁ ↑S₂),
   ∀ (m : M₁.M.univ), ∃ (m': M₂.M.univ),
   ∃ (η' : extend_struc_by_element S₁ m → extend_struc_by_element S₂ m'),
   η' is_isomorphism ∧ (η' m = m') ∧ (η = η' on S₁)