proposition: Lemma expr_compare_eq_dep n m (x: expr n m): forall p q (y: expr p q), expr_compare x y = Eq -> n=p -> m=q -> eq_dep (I*I) (fun x => expr (fst x) (snd x)) (n,m) x (p,q) y.
proof: Proof. induction x; intros ? ? z C; destruct z; try discriminate C; try (intros <- <- || intros <- _); try reflexivity; simpl expr_compare in C. apply compare_lex_eq in C as [C1 C2]. apply IHx1, cmp_eq_dep_eq in C1; trivial. apply IHx2, cmp_eq_dep_eq in C2; trivial. subst. reflexivity. apply compare_lex_eq in C as [C1 C2]. apply IHx1, cmp_eq_dep_eq in C1; trivial. apply IHx2, cmp_eq_dep_eq in C2; trivial. subst. reflexivity. apply IHx, cmp_eq_dep_eq in C; trivial. subst. reflexivity. apply compare_lex_eq in C as [C C']. apply cmp_eq in C. subst. apply compare_lex_eq in C' as [C1 C2]. apply IHx1, cmp_eq_dep_eq in C1; trivial. apply IHx2, cmp_eq_dep_eq in C2; trivial. subst. reflexivity. apply IHx, cmp_eq_dep_eq in C; trivial. subst. reflexivity. apply IHx, cmp_eq_dep_eq in C; trivial. subst. reflexivity. apply IHx, cmp_eq_dep_eq in C; trivial. subst. reflexivity. apply compare_lex_eq in C as [C C']. apply cmp_eq in C. subst. apply compare_lex_eq in C' as [C1 C2]. apply IHx1, cmp_eq_dep_eq in C1; trivial. apply IHx2, cmp_eq_dep_eq in C2; trivial. subst. reflexivity. apply compare_lex_eq in C as [C C']. apply cmp_eq in C. subst. apply compare_lex_eq in C' as [C1 C2]. apply IHx1, cmp_eq_dep_eq in C1; trivial. apply IHx2, cmp_eq_dep_eq in C2; trivial. subst. reflexivity. apply cmp_eq in C. subst. reflexivity. Qed.
imports: positives comparisons Eqdep monoid