#src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst
#a1 #a2 #Hcursrc #Hcurdst #Hsep
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
[ whd in match (trans ????);
>Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
| whd in match (trans ????);
#src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst
#a1 #a2 #Hcursrc #Hcurdst #Hsep
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
[ whd in match (trans ????);
>Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
| whd in match (trans ????);