(3steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: decidable spread 1 1
1. T: Type
2. U: Type
3. P: TUProp
4. x:T, y:U. Dec(P(x,y))
5. p1: T
6. p2: U

Dec(P(p1,p2))
By:
HypBackchain
THEN
Trivial
Generated subgoals:

None

About:
decidablefunctionuniversepropall

(3steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc