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