proposition: Lemma DeqSym: forall {A} T (deq : Deq A) (a b: A) (f : (a=b) -> T) (c:T), match deq a b with | left p => f p | _ => c end = match deq b a with | left p => f (eq_sym p) | _ => c end.
proof: Proof. intros. destruct (deq a b) as [HH| HH]. - destruct (deq a b) as [H| H]; subst;sp. destruct (deq b b); sp;[]. pose proof (UIPReflDeq deq _ e) as XX. rw XX. auto. - destruct (deq b a) as [H| H]; subst; sp. Defined.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega Coq.Logic.Eqdep_dec