proposition: Lemma t0_empty (alpha: t 0): False.
proof: Proof. destruct alpha ; discriminate. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)