proposition: Lemma singletonSubst_conv T T' G G' Q : isSingletonSubst T G -> isSingletonSubst T' G' -> G ~~(Q) G' -> T ~(Q) T'.
proof: Proof. intros. destruct H; destruct H0; destruct H1. assert (Q00: envSub Q 0 0). destruct (sc_inj_l0 0 T H). destruct x; trivial. destruct (sc_lr0 0 (S x) T H1 H) as [W [G'W _]]. destruct (H3 x); inversion G'W; try_solve. destruct (sc_lr0 0 0 T Q00 H) as [T'' [G'T'' TT'']]. assert (T'T'': T' = T''). inversion H0; inversion G'T''; destruct G'; try_solve. rewrite T'T''; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)