(8steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: rel-graph functionality 1
1. T: Type
2. R1: TTProp
3. R2: TTProp
4. x,y:T. R1(x,y) R2(x,y)
Id {p:(TT)| R1(1of(p),2of(p)) }{p:(TT)| R2(1of(p),2of(p)) }
By:
Unfold `identity` 0
THEN
ParallelOp -1
THEN
EasyHyp
Generated subgoals:

None

About:
productsetfunctionuniversememberpropall

(8steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc