have s1 : Function.LeftInverse σ' σ.1 := congr_fun a1_right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ Function.Injective ↑σ
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.LeftInverse σ' ↑σ
⊢ Function.Injective ↑σ