proposition: Fact mma_sss_fun i s t1 t2 : i // s -1> t1 -> i // s -1> t2 -> t1 = t2.
proof: Proof. intros []; subst. + inversion 1; subst; auto. + inversion 1; subst; auto. rewrite H in H6; discriminate. + inversion 1; subst; auto. * rewrite H in H6; discriminate. * rewrite H in H6; inversion H6; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)