Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. f:{T}. (x,y,z:T. (f x y) (f y z) (f x z)) (x,y:T. (f x y) (f y x)) (x:T. (f x x)) f T T


Applied Tactic: ProvePropertiesLemma
Generated subgoals:

1. (f x z)

2. (f y x)

3. (f x y)

4. (f x x)