Use named hypothesis

Author: Linyxus

Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean

@@ -32,9 +32,13 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax
     must preserve the variable and type bindings in the context. -/
 structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where
   /-- Term variable preservation: x:T in Γ implies f(x):f(T) in Δ -/
-  var : ∀ x T, Ctx.LookupVar Γ x T → Ctx.LookupVar Δ (f.var x) (T.rename f)
+  var : ∀ x T,
+    (hb : Ctx.LookupVar Γ x T) →
+    Ctx.LookupVar Δ (f.var x) (T.rename f)
   /-- Type variable preservation: X<:T in Γ implies f(X)<:f(T) in Δ -/
-  tvar : ∀ X T, Ctx.LookupTVar Γ X T → Ctx.LookupTVar Δ (f.tvar X) (T.rename f)
+  tvar : ∀ X T,
+    (hb : Ctx.LookupTVar Γ X T) →
+    Ctx.LookupTVar Δ (f.tvar X) (T.rename f)
 
 /-- **Lifting rebinding morphisms over term variable binders**.
 

Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean

@@ -31,8 +31,12 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSyste
 
     Unlike rebinding morphisms, retyping morphisms map variables to typing derivations. -/
 structure Retype (Γ : Ctx s1) (σ : Subst s1 s2) (Δ : Ctx s2) where
-  var : ∀ x T, Γ.LookupVar x T → HasType Δ (σ.var x) (T.subst σ)
-  tvar : ∀ X S, Γ.LookupTVar X S → Subtyp Δ (σ.tvar X) (S.subst σ)
+  var : ∀ x T,
+    (hb : Γ.LookupVar x T) →
+    HasType Δ (σ.var x) (T.subst σ)
+  tvar : ∀ X S,
+    (hb : Γ.LookupTVar X S) →
+    Subtyp Δ (σ.tvar X) (S.subst σ)
 
 /-- Extends a retyping morphism to contexts with an additional term variable. -/
 def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P.subst σ) where