At:
rel-graph functionality3
1.
T: Type
2.
R1: TTProp
3.
R2: TTProp
4.
x,y:T. R1(x,y) R2(x,y)
(Id,Id) o Id = Id o Id {p:(TT)| R1(1of(p),2of(p)) }TT
By:
ExtWith [`z'] [TTTT]
THEN
Reduce 0
THEN
Analyze -1
THEN
Analyze -2
THEN
Reduce 0
Generated subgoals:
T
x,y:T. R1(x,y) 
R2(x,y)
(Id,Id) o Id = Id o Id 
{p:(T
T)| R1(1of(p),2of(p)) }