take {} (Vars,(QuasiTerms C)) ; :: thesis: {} (Vars,(QuasiTerms C)) is empty
thus {} (Vars,(QuasiTerms C)) is empty ; :: thesis: verum