take Trivial-AMI N ; :: thesis: Trivial-AMI N is IC-Ins-separated
thus Trivial-AMI N is IC-Ins-separated ; :: thesis: verum