PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux6 quo 1 1
1. T: Type
2. R: TTProp
3. EquivRel x,y:T. x R y
4. Q: (x,y:T//(x R y))(x,y:T//(x R y))Prop

Refl(x,y:T//(x R y);u,v.u Q v) & Sym u,v:x,y:T//(x R y). u Q v & Trans u,v:x,y:T//(x R y). u Q v Refl(T;x,y.x Q y) & Sym x,y:T. x Q y & Trans x,y:T. x Q y
By: Unfolds [`refl`;`sym`;`trans`] 0
Generated subgoal:

1 (a:x,y:T//(x R y). a Q a) & (a,b:x,y:T//(x R y). (a Q b) (b Q a)) & (a,b,c:x,y:T//(x R y). (a Q b) (b Q c) (a Q c)) (a:T. a Q a) & (a,b:T. (a Q b) (b Q a)) & (a,b,c:T. (a Q b) (b Q c) (a Q c))

About:
impliesandquotientuniversefunctionpropall