proposition: Lemma singletonSubst_conv_rev T T' G G' Q : isSingletonSubst T G -> isSingletonSubst T' G' -> envSub Q 0 0 -> T ~(Q) T' -> G ~~(Q) G'.
proof: Proof. intros. destruct H; destruct H0. constructor; intros. destruct x; destruct y. exists T'; split; trivial. assert (T = T0). inversion H; inversion H6; try_solve. rewrite <- H7; trivial. absurd (S y = 0); [lia | apply envSub_Lok with Q 0; trivial]. absurd (S x = 0); [lia | apply envSub_Rok with Q 0; trivial]. destruct (H3 x); inversion H6; try_solve. destruct x; destruct y. exists T; split; trivial. assert (T'0 = T'). inversion H0; inversion H6; try_solve. rewrite H7; trivial. absurd (S y = 0); [lia | apply envSub_Lok with Q 0; trivial]. absurd (S x = 0); [lia | apply envSub_Rok with Q 0; trivial]. destruct (H4 y); inversion H6; try_solve. destruct x. exists 0; trivial. destruct (H3 x); inversion H5; try_solve. destruct y. exists 0; trivial. destruct (H4 y); inversion H5; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)