proposition: Theorem beq_var_false_not_eq : forall i1 i2, beq_var i1 i2 = false -> i1 <> i2.
proof: Proof. intros. destruct i1; destruct i2. unfold beq_var in H. apply beq_nat_false_iff in H. intro; apply H; inversion H0; auto. Defined.
imports: list Omega