proposition: Lemma one_less_length : forall l l', one_less l l' -> length l = length l'.
proof: Proof. intro l; induction l as [ | h t IHl]; intros l' Hr. inversion Hr; subst. simpl; trivial. inversion Hr; subst; simpl. destruct p as [ | p]. simpl; trivial. simpl; rewrite IHl with (t[p:=a']); trivial. apply (@one_less_cons t (t[p:=a']) p a a'); trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)