cases a1
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
case intro
σ : Instantiation
σ' : VarName → VarName
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id