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