take TotalTRS (NAT,(In (0,NAT))) ; :: thesis: ( TotalTRS (NAT,(In (0,NAT))) is strict & TotalTRS (NAT,(In (0,NAT))) is quasi_total & TotalTRS (NAT,(In (0,NAT))) is partial & TotalTRS (NAT,(In (0,NAT))) is Group-like & TotalTRS (NAT,(In (0,NAT))) is invariant )
thus ( TotalTRS (NAT,(In (0,NAT))) is strict & TotalTRS (NAT,(In (0,NAT))) is quasi_total & TotalTRS (NAT,(In (0,NAT))) is partial & TotalTRS (NAT,(In (0,NAT))) is Group-like & TotalTRS (NAT,(In (0,NAT))) is invariant ) ; :: thesis: verum