reconsider l = I[01] --> t as constant Loop of t by JORDAN:41;
take l ; :: thesis: l is constant
thus l is constant ; :: thesis: verum