proposition: Lemma alien_sub_var : forall x, alien_sub (Var x) x = Var x.
proof: Proof. intro. unfold alien_sub, fsub. simpl. case (le_lt_dec x x). auto. intro. absurd (x < x). apply Nat.lt_irrefl. hyp. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)