Thm* q:. (q*) ~ list_1_1_nat
Thm* P,Q:(TProp). (t:T. P(t) Q(t)) ({t:T| P(t) } ~ {t:T| Q(t) }) auto2_lemma_1
In prior sections: fun 1 finite sets
q:
. (q*) ~ list_1_1_nat
f:(A
B), g:(BA). InvFuns(A; B; f; g)
q:. (q*) ~ list_1_1_nat
P,Q:(TProp). (t:T. P(t) 
Q(t)) 
({t:T| P(t) } ~ {t:T| Q(t) })
auto2_lemma_1