proposition: Lemma is_unit_of_Unit : forall i j : idx, is_unit_of i j = true -> Unit R (Bin.value (e_bin i)) (eval (unit j)).
proof: Proof. intros. unfold is_unit_of in H. rewrite existsb_exists in H. destruct H as [x [H H']]. revert H' ; case (eq_idx_spec); [intros H' _ ; subst| intros _ H'; discriminate]. simpl. destruct x. simpl. auto. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)