#n #c1 #c2 * #ri1 #rs1 #H destruct
#H elim (eq_t_inv_dx … H) -H /2 width=3 by ex1_2_intro/
qed-.
(* Basic inversion properties ***********************************************)
#n #c1 #c2 * #ri1 #rs1 #H destruct
#H elim (eq_t_inv_dx … H) -H /2 width=3 by ex1_2_intro/
qed-.
(* Basic inversion properties ***********************************************)