apply Exists.intro σ.1
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ ∃ σ'_1, σ' ∘ σ'_1 = id ∧ σ'_1 ∘ σ' = id
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id ∧ ↑σ ∘ σ' = id