proposition: Lemma safe_poly_type_eqE {n n' ts ts' x x'} : safe_poly_type n ts x = safe_poly_type n' ts' x' -> n = n' /\ ts = ts' /\ x = x'.
proof: Proof. elim: n n' x x'. - move=> [|?]; last by case: ts. move=> x x'. elim: ts ts'. + case; last done. by move=> []. + move=> ? ? IH. case; first done. by move=> ? ? [] <- /IH [_] [<-] <-. - move=> n IH [|n']; first by case: (ts'). move=> x x' []. have -> : S (n + x) = n + (S x) by lia. have -> : S (n' + x') = n' + (S x') by lia. by move=> /IH [->] [->] [->]. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun