There seams to be subtle differences between how the two inductive principles are set up in Coq vs Pie

show-how-equality-induction-works.rkt

#lang pie

(claim +
  (-> Nat Nat
    Nat))

(define +
  (λ (a b)
    (rec-Nat a
      b
      (λ (_ h)
        (add1 h)))))

(claim double
  (-> Nat
      Nat))

(define double (lambda (n) (+ n n)))
  
(claim plus_id_ex
  (Pi ((n Nat)
       (m Nat))
    (-> (= Nat n m) (= Nat (+ n n) (+ m m)))))

(define plus_id_ex
  (lambda (n m n=m) ;; This is the same as `fun (n m: nat) (H : n = m)`
    #;;This is enough
    (cong n=m double)

    #;;This also works
    (replace n=m
      (lambda (m0) (= Nat (+ n n) (+ m0 m0)))
      (same (+ n n)))

    (ind-= n=m ;; This is the same as `eq_ind`,
               ;; except it accepts the Prop as argument instead of the nat
      (lambda (m0 _) (= Nat (+ n n) (+ m0 m0))) ;; This is the same motive
      (same (+ n n))))) ;; this is the same as `eq_refl`

;plus_id_ex =
;fun (n m : nat) (H : n = m) => eq_ind n (fun m0 : nat => n + n = m0 + m0) eq_refl m H
;     : forall n m : nat, n = m -> n + n = m + m