∀[P:ℙ]. (SqStable(P) 
 P supposing P)
{ Auto }
1. [P] : ℙ
2. SqStable(P)@i
3. [%1] : P
⊢ P
2. P supposing P@i
⊢ SqStable(P)