Function lemma_tail_and_then_consistent 

pub broadcast proof fn lemma_tail_and_then_consistent<Then>(then: Then, v: Then::Val)
where
    Then: Consistency + SpecByteLen<T = Then::Val>,

ensures

#[trigger] super::AndThen(Tail, then).consistent(v) == then.consistent(v),