(4steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: sq stable list all


T:Type, P:(TProp), L:T List. (x:T. SqStable(P(x))) SqStable(xL.P(x))

By: UnivCD

Generated subgoal:

11. T: Type
2. P: TProp
3. L: T List
4. x:T. SqStable(P(x))
SqStable(xL.P(x))

About:
listfunctionuniversepropimpliesall

(4steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc