PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 1 1 1 2 2 1 1 1
1. T: Type
2. P: TProp
3. Q: TProp
4. t:T. P(t) Q(t)

(x.x) = Id & (x.x) = Id
By: Fold `identity` 0
Generated subgoal:

1 Id = Id & Id = Id

About:
andequalfunctionsetapply
lambdauniversepropall