take Trivial-AMI IL,E ; :: thesis: Trivial-AMI IL,E is strict
thus Trivial-AMI IL,E is strict ; :: thesis: verum