set f = the non constant FinSequence;
take the non constant FinSequence ; :: thesis: not the non constant FinSequence is constant
thus not the non constant FinSequence is constant ; :: thesis: verum