proposition: Lemma true_Cne_neq: forall x y, typed_true tint (force_val (sem_cmp_pp Cne (pointer_val_val x) (pointer_val_val y))) -> x <> y.
proof: Proof. intros. hnf in H. destruct x, y; inversion H; [|intro; inversion H0..]. simpl in H. clear H1. unfold sem_cmp_pp in H. simpl in H. destruct (eq_block b b0). - destruct (Ptrofs.eq i i0) eqn:? . + simpl in H. inversion H. + subst b0. pose proof (Ptrofs.eq_spec i i0). rewrite Heqb1 in H0. intro; apply H0. inversion H1. reflexivity. - intro. inversion H0. auto. Qed.
imports: CertiGraph.unionfind.env_unionfind CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList CertiGraph.msl_application.GList_UnionFind CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_graph_glist