codatatypes and least predicates in Dafny. Does it make any sense?

I am trying to deal with infinite lists as follows:

codatatype iList = iCons(head: int, tail: iList)

least predicate isIn(e: int, l: iList)
{
  e == l.head || isIn(e, l.tail)
}

least predicate allThrees(input: iList)
{
  input.head == 3 && allThrees(input.tail)
}

least lemma Check1_Lemma(input: iList)
  requires allThrees(input)
  ensures forall b: int :: isIn(b, input) ==> b == 3
{}

I use "least predicates" instead of "greatest predicates" because it allows me to prove many more properties. However, something is wrong with this. If I define the predicate:

least predicate aValidInput(input: iList)
{
  0 <= input.head && input.head <= 3 && aValidInput(input.tail)
}

and try to prove this lemma:

least lemma Check2_Lemma(input: iList)
  requires allThrees(input)
  ensures aValidInput(input)
{} 

I realize that it is also possible to prove the contrary:

least lemma Check3_Lemma(input: iList)
  requires allThrees(input)
  ensures ! aValidInput(input)
{} 

So, is the problem the use of "least predicate"? But with "greatest predicates" I am not able to prove these naive lemmas.

Consider following snippet.

least lemma IsFalse(input: iList)
  requires aValidInput(input)
  ensures false
{} 

Given aValidInput, false is provable. This means aValidInput is never true. Dafny uses prefix predicates to define least and greatest predicate. For least predicate it means there is ordinal k_ for which prefix predicate is true. Please look into section Working with Extreme Predicates of paper. If you unroll definition of prefixes of least predicates for aValidInput, you will see it is always false. (Base case k_ = 0 is always false (by definition) and successive case k_ takes && with expression 0 <= input.head && input.head <= 3 and previous case k_ - 1. Hence by induction it is always false.)

I believe isIn is doing right thing of using least predicate as it is true when there exists ordinal k_ such that unfolding stream k_ times you get an element which is equal to e. But use of least predicate for aValidInput is problematic as you want to say that for any number of unfolding of stream, all its elements are between 0 and 3. Notice difference between there exists unfolding up to and any number of unfolding. Hence correct definition should be following

greatest predicate allThrees(input: iList)
{
  input.head == 3 && allThrees(input.tail)
}

greatest predicate aValidInput(input: iList)
{
  0 <= input.head && input.head <= 3 && aValidInput(input.tail)
}

greatest lemma Check2_Lemma(input: iList)
  requires allThrees(input)
  ensures aValidInput(input)
{} 

greatest lemma Check3_Lemma(input: iList)
  requires allThrees(input)
  ensures ! aValidInput(input)
{} 

Another way to say is for predicate like isIn when element is equal to e one doesn't have to look further hence least predicate works, where as for predicate like allThrees and aValidInput even if current element satisfies conditions, rest of stream need to be checked hence one should use greatest predicate.

Edit: Just noticed Dafny can't prove Check1_Lemma automatically now. It can be proved by following way.

lemma Check1_Lemma_Aux(k: ORDINAL, b: int, input: iList)
  decreases k
  requires allThrees(input)
  requires isIn#[k](b, input)
  ensures b == 3
{
  if k == 0 {}
  else if k.IsLimit {}
  else {
    if isIn#[k-1](b, input.tail) {
      Check1_Lemma_Aux(k-1, b, input.tail);
    }
    else {}
  }
}

lemma Check1_Lemma(input: iList)
  requires allThrees(input)
  ensures forall b: int :: isIn(b, input) ==> b == 3
{
   forall b: int | isIn(b, input) ensures b == 3 {
      if(isIn(b, input)){ 
        var k :| isIn#[k](b, input);
        Check1_Lemma_Aux(k, b, input);
      }
   }
}