PROOF EDITOR

pq   ⊢  
α1(1)pq A
α1(Z)
Next action